\begin{tabbing}
$\forall$\=${\it es}$:ES, $P_{1}$, $Q_{1}$, $P_{2}$, $Q_{2}$:(E$\rightarrow\mathbb{P}$), ${\it dcd\_P}_{1}$:($e$:E$\rightarrow$Dec($P_{1}$($e$))), $f$:(\{$e$:E$\mid$ $P_{1}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{1}$($e$)\} ),\+
\\[0ex]$g$:(\{$e$:E$\mid$ $P_{2}$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q_{2}$($e$)\} ).
\-\\[0ex]($\forall$$e$:E. ($P_{1}$($e$)) $\Rightarrow$ ($\neg$($P_{2}$($e$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($Q_{1}$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($Q_{2}$($e$)))
\\[0ex]$\Rightarrow$ $Q_{1}$ $\leftarrow\leftarrow$= $f$== $P_{1}$
\\[0ex]$\Rightarrow$ $Q_{2}$ $\leftarrow\leftarrow$= $g$== $P_{2}$
\\[0ex]$\Rightarrow$ $Q_{1}$ $\vee$ $Q_{2}$ $\leftarrow\leftarrow$= [$P_{1}$? $f$ : $g$]== $P_{1}$ $\vee$ $P_{2}$
\end{tabbing}